(* $Id: ergo.ml 226 2009-03-11 16:04:17Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

open PFOLSyntax
open PFOLSyntax.Raw
open ErgoPrinter
open Options
open Arg

type options = {
  mutable timeout : int;
}

let options = { timeout = 1800; }

let remove = ref false
let dir = ref None

let ergo_command () =
  Printf.sprintf "%s %d %s -triggers-var -redondance 5"
    Configuration.timeout (1 + options.timeout / 20) Configuration.ergo

let ergo_notriggers_command () =
  Printf.sprintf "%s %d %s"
    Configuration.timeout options.timeout Configuration.ergo

let options () =
  mk_local_options
    {
      env = options;
      postprocess = (fun x -> x);
      options = Arg.align [
        "--timeout", Int (fun x -> options.timeout <- x),
        " Specify number of seconds after which to timeout Ergo proofs [default = 1800]."
      ]
    }

module C = Misc.Cache
  (struct type t = string * string
	  let hash (_, g) = Hashtbl.hash g
	  let equal (f1, g1) (f2, g2) =
	    String.compare g1 g2 = 0 && String.compare f1 f2 = 0
   end)
  (struct type t = bool * string end)

let cache_fun = ref (fun f x -> f x)
let close_fun = ref ignore

let init_cache filename =
  let (cache, close) = C.cache_in_file filename in
    cache_fun := cache;
    close_fun := close

let save_cache () =
  !close_fun ()

let if_not_removed remove filename =
  if remove then "" else "(filename: "^ filename ^")"

let cp_to_dir filename =
  match !dir with
    | None -> filename
    | Some dir ->
	ignore (Sys.command (Printf.sprintf "cp %s %s" filename dir));
	Filename.concat dir (Filename.basename filename)

let launch_ergo command matching_output q =
  Misc.tmp_filename_from_string ~remove:!remove ".mlw"
    q
    (fun filename ->
(*       Printf.printf "cmd: %s %s\n%!" (command ()) filename; *)
       match
	 Sys.command
	   (Printf.sprintf
	      "(%s %s | grep \"%s\") 1> /dev/null 2> /dev/null"
	      (command ())
	      filename
	      matching_output)
       with
	 | 0 -> (true, if_not_removed !remove (cp_to_dir filename))
	 | _ -> (false, if_not_removed !remove (cp_to_dir filename)))


let inconsistent_assumptions (q, _) =
  match launch_ergo ergo_command "Valid" q with
    | (false, _) -> launch_ergo ergo_notriggers_command "Valid" q
    | r -> r

let prove (q, _) =
  match launch_ergo ergo_command "Valid" q with
    | (false, _) -> launch_ergo ergo_notriggers_command "Valid" q
    | r -> r

let tries = ref 0
let success = ref 0

let prove with_split q odir =
  dir := odir;
  incr tries;
  let (ret, filename) = !cache_fun prove (print with_split q) in
    if ret then incr success;
    (ret, filename)

let inconsistent_assumptions q odir =
  dir := odir;
  let (qr, g) = print true q in
  let (ret, filename) =
    !cache_fun inconsistent_assumptions
      ("(* Look for inconsistent_assumption *)\n" ^ qr, g)
  in
    if not ret then
      prove true q odir
    else
      (ret, filename)

let print_stats () =
  Printf.printf "Ergo made %d proofs (%d requests).\n"
    !success !tries
